\begin{tabbing}
$\forall$${\it the\_w}$:World.
\\[0ex]FairFifo
\\[0ex]$\Rightarrow$ (\=$\forall$$e$:E, $l$:IdLnk, $n$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$sends($l$;$e$)$\parallel$}}$.\+
\\[0ex]$\exists$${\it e'}$:E. isrcv(kind(${\it e'}$)) \& lnk(kind(${\it e'}$)) $=$ $l$ \& sender(${\it e'}$) $=$ $e$ \& index(${\it e'}$) $=$ $n$ $\in$ $\mathbb{Z}$)
\-
\end{tabbing}